$\forall$$i$:Id, $R$:Realizer.
\\[0ex]$\neg$Rplus?($R$) $\Rightarrow$ $\neg$Rnone?($R$) $\Rightarrow$ R{-}da($R$;$i$) $=$ if R{-}loc($R$) = $i$$\rightarrow$ Rda($R$) else  fi $\in$ $x$:Knd fp$\rightarrow$ Type